Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		plus(s(s(x)),y)	→ s(plus(x,s(y)))
2:		plus(x,s(s(y)))	→ s(plus(s(x),y))
3:		plus(s(0),y)	→ s(y)
4:		plus(0,y)	→ y
5:		ack(0,y)	→ s(y)
6:		ack(s(x),0)	→ ack(x,s(0))
7:		ack(s(x),s(y))	→ ack(x,plus(y,ack(s(x),y)))

There are 6 dependency pairs:


8:		PLUS(s(s(x)),y)	→ PLUS(x,s(y))
9:		PLUS(x,s(s(y)))	→ PLUS(s(x),y)
10:		ACK(s(x),0)	→ ACK(x,s(0))
11:		ACK(s(x),s(y))	→ ACK(x,plus(y,ack(s(x),y)))
12:		ACK(s(x),s(y))	→ PLUS(y,ack(s(x),y))
13:		ACK(s(x),s(y))	→ ACK(s(x),y)

The approximated dependency graph contains 2 SCCs: {8,9} and {10,11,13}.

Consider the SCC {8,9}. There are no usable rules. The constraints could not be solved.

Consider the SCC {10,11,13}. The constraints could not be solved.

Tyrolean Termination Tool (0.04 seconds) --- May 3, 2006